

Checking transition consistency


msc diagrams: three_way_connect(32) and CW_answer(23)
INCONSISTENCY:
Matching formula: k32 = k23
Precondition 1: rel (m32 , k32 , connected) & rel (k32 , n32 , three_wayhold); Precondition 2: state (n23 , ringing k23) & rel (k23 , m23 , connected);
Post condition 1: rel (m32 , n32 , three_wayconnected k32); Post condition 2: rel (k23 , m23 , cw hold connect n23);

msc diagrams: three_way_initial(29) and CW_answer(23)
INCONSISTENCY:
Matching formula: m29 = k23
Precondition 1: rel (m29 , n29 , connected) & Forall k (~(rel (m29 , k , three_wayhold))); Precondition 2: state (n23 , ringing k23) & rel (k23 , m23 , connected);
Post condition 1: state (m29 , dial) & rel (m29 , n29 , three_wayhold); Post condition 2: rel (k23 , m23 , cw hold connect n23);

msc diagrams: three_way_teardown1(28) and three_way_teardown2(25)
INCONSISTENCY:
Matching formula: m28 = k25
Precondition 1: rel (m28 , n28 , three_wayconnected k28); Precondition 2: rel (m25 , n25 , three_wayconnected k25);
Post condition 1: rel (n28 , k28 , connected); Post condition 2: state (m25 , dial) & state (n25 , dial);

msc diagrams: three_way_teardown1(28) and CW_teardown1(20)
INCONSISTENCY:
Matching formula: m28 = m20
Precondition 1: rel (m28 , n28 , three_wayconnected k28); Precondition 2: rel (k20 , n20 , cw hold connect m20);
Post condition 1: rel (n28 , k28 , connected); Post condition 2: rel (k20 , n20 , connected);

msc diagrams: three_way_teardown1(28) and CW_teardown2(18)
INCONSISTENCY:
Matching formula: m28 = m18
Precondition 1: rel (m28 , n28 , three_wayconnected k28); Precondition 2: rel (k18 , m18 , cw hold connect n18);
Post condition 1: rel (n28 , k28 , connected); Post condition 2: rel (k18 , n18 , cw hold);

msc diagrams: three_way_teardown1(28) and CW_teardown3(15)
INCONSISTENCY:
Matching formula: m28 = k15
Precondition 1: rel (m28 , n28 , three_wayconnected k28); Precondition 2: rel (k15 , n15 , cw hold connect m15);
Post condition 1: rel (n28 , k28 , connected); Post condition 2: state (m15 , dial) & state (n15 , dial);

msc diagrams: three_way_teardown2(25) and CW_teardown1(20)
INCONSISTENCY:
Matching formula: k25 = m20
Precondition 1: rel (m25 , n25 , three_wayconnected k25); Precondition 2: rel (k20 , n20 , cw hold connect m20);
Post condition 1: state (m25 , dial) & state (n25 , dial); Post condition 2: rel (k20 , n20 , connected);

msc diagrams: three_way_teardown2(25) and CW_teardown2(18)
INCONSISTENCY:
Matching formula: k25 = m18
Precondition 1: rel (m25 , n25 , three_wayconnected k25); Precondition 2: rel (k18 , m18 , cw hold connect n18);
Post condition 1: state (m25 , dial) & state (n25 , dial); Post condition 2: rel (k18 , n18 , cw hold);

msc diagrams: three_way_teardown2(25) and CW_teardown3(15)
INCONSISTENCY:
Matching formula: k25 = k15
Precondition 1: rel (m25 , n25 , three_wayconnected k25); Precondition 2: rel (k15 , n15 , cw hold connect m15);
Post condition 1: state (m25 , dial) & state (n25 , dial); Post condition 2: state (m15 , dial) & state (n15 , dial);

msc diagrams: three_way_teardown3(24) and CW_switch2(21)
INCONSISTENCY:
Matching formula: m24 = k21
Precondition 1: state (m24 , dial) & rel (m24 , n24 , three_wayhold); Precondition 2: rel (k21 , m21 , cw hold);
Post condition 1: rel (m24 , n24 , connected); Post condition 2: rel (k21 , m21 , connected);

msc diagrams: CW_switch1(22) and CW_teardown2(18)
INCONSISTENCY:
Matching formula: k22 = k18
Precondition 1: rel (k22 , m22 , cw hold connect n22); Precondition 2: rel (k18 , m18 , cw hold connect n18);
Post condition 1: rel (k22 , n22 , cw hold connect m22); Post condition 2: rel (k18 , n18 , cw hold);